box!(${\it Run}$;$P$)(${\it sys}$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$($\exists$${\it run}$:${\it Run}$. ${\it sys}$(${\it run}$)) \& ($\forall$${\it run}$:${\it Run}$. ${\it sys}$(${\it run}$) $\Rightarrow$ $P$(${\it run}$))